Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, still suffer from the state space explosion problem that makes them impractical for large scale systems and/or specifications. In this paper, we propose to use graph representation learning (GRL) for solving linear temporal logic (LTL) model checking, where the system and the specification are expressed by a B\"uchi automaton and an LTL formula respectively. A novel GRL-based framework OCTAL, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification in the latent space. The empirical experiments show that OCTAL achieves comparable accuracy against canonical SOTA model checkers on three different datasets, with up to $5\times$ overall speedup and above $63\times$ for satisfiability checking alone.

Concurrent systems identify systems, either software, hardware or even biological systems, that are characterized by sets of independent actions that can be executed in any order or simultaneously. Computer scientists resort to a causal terminology to describe and analyse the relations between the actions in these systems. However, a thorough discussion about the meaning of causality in such a context has not been developed yet. This paper aims to fill the gap. First, the paper analyses the notion of causation in concurrent systems and attempts to build bridges with the existing philosophical literature, highlighting similarities and divergences between them. Second, the paper analyses the use of counterfactual reasoning in ex-post analysis in concurrent systems (i.e. execution trace analysis).